p,q:. (p =b q)  (p = q) 

latex

ProofTree

Definitions	t  T, x:A. B(x), p =b q, , P  Q, P  Q, P  Q, True, ff, if b then t else f fi , tt, b, p  q, p q, b, P  Q, False, Unit, , A,
Lemmas	bool wf, bfalse wf, false wf, btrue wf, true wf, btrue neq bfalse